Inference at * 1 
Iof proof for Lemma p-compose' wf:



1. A : Type
2. B : Type
3. C : Type
4. g : A(B + Top)
5. ABC
6. x : A
7. (can-apply(g;x))
  g(x)  (C + Top) 

latex

 by (MoveToConcl (-1)) 
CollapseTHEN ((Unfold `can-apply` ( 0)) 
CollapseTHEN (((
CGenConclAtAddr [1;1;1;1]) 
CollapseTHENA (Auto)) 
CollapseTHEN ((D (-2)) 
CollapseTHEN ((
CReduce 0) 
CollapseTHEN (Auto))))) 

latex

C.

Definitions	can-apply(f;x), s = t, f(a), left + right, inl x , Top, x:AB(x), True, b, P  Q, inr x , A, x:A. B(x), t  T, False
Lemmas	true wf, not wf, false wf